1  /-
  2  Copyright (c) 2018 Kenny Lau. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Author: Kenny Lau
  5  
  6  The perfect closure of a field.
  7  -/
  8  
  9  import algebra.char_p
src         └────────────┘
 10  
 11  universes u v
 12  
 13  /-- A perfect field is a field of characteristic p that has p-th root. -/
 14  class perfect_field (α : Type u) [field α] (p : ℕ) [char_p α p] : Type u :=
id                            └──┘     └───┘           └────┘  
src                                    └───┘            └────┘
typ                           └──┘     └───┘           └────┘  
doc                                                      └────┘
 15  (pth_root : α → α)
id                 
typ                
 16  (frobenius_pth_root : ∀ x, frobenius α p (pth_root x) = x)
id                             └───────┘    └──────┘    
src                             └───────┘                  
typ                            └───────┘    └──────┘    
doc                             └───────┘
 17  
 18  theorem frobenius_pth_root (α : Type u) [field α] (p : ℕ) [char_p α p] [perfect_field α p] (x : α) :
id                                            └───┘           └────┘     └───────────┘         
src                                           └───┘            └────┘       └───────────┘
typ                                           └───┘           └────┘     └───────────┘         
doc                                                             └────┘       └───────────┘
 19    frobenius α p (perfect_field.pth_root p x) = x :=
id     └───────┘    └────────────────────┘     
src    └───────┘      └────────────────────┘      
typ    └───────┘    └────────────────────┘     
doc    └───────┘
 20  perfect_field.frobenius_pth_root p x
id   └──────────────────────────────┘  
src  └──────────────────────────────┘
typ  └──────────────────────────────┘  
 21  
 22  theorem pth_root_frobenius (α : Type u) [field α] (p : ℕ) [nat.prime p] [char_p α p] [perfect_field α p] (x : α) :
id                                            └───┘           └───────┘    └────┘     └───────────┘         
src                                           └───┘            └───────┘     └────┘       └───────────┘
typ                                           └───┘           └───────┘    └────┘     └───────────┘         
doc                                                             └───────┘     └────┘       └───────────┘
 23    perfect_field.pth_root p (frobenius α p x) = x :=
id     └────────────────────┘   └───────┘      
src    └────────────────────┘    └───────┘        
typ    └────────────────────┘   └───────┘      
doc                              └───────┘
 24  frobenius_inj α p _ _ (by rw frobenius_pth_root)
id   └───────────┘              └────────────────┘
src  └───────────┘             └─┘└────────────────┘
typ  └───────────┘           └─┘└────────────────┘
doc                            └─┘
txt                            └─┘
par                            └─┘
pid                              
st                            └────────────────────┘
 25  
 26  instance pth_root.is_ring_hom (α : Type u) [field α] (p : ℕ) [nat.prime p] [char_p α p] [perfect_field α p] :
id                                               └───┘           └───────┘    └────┘     └───────────┘  
src                                              └───┘            └───────┘     └────┘       └───────────┘
typ                                              └───┘           └───────┘    └────┘     └───────────┘  
doc                                                                └───────┘     └────┘       └───────────┘
 27    is_ring_hom (@perfect_field.pth_root α _ p _ _) :=
id     └─────────┘   └────────────────────┘    
src    └─────────┘   └────────────────────┘
typ    └─────────┘   └────────────────────┘    
doc    └─────────┘
 28  { map_one := frobenius_inj α p _ _ (by rw [frobenius_pth_root, frobenius_one]),
id                └───────────┘               └────────────────┘  └───────────┘
src               └───────────┘             └──┘└────────────────┘└┘└───────────┘
typ               └───────────┘           └──┘└────────────────┘└┘└───────────┘
doc                                         └──┘                  └┘             
txt                                         └──┘                  └┘             
par                                         └──┘                  └┘             
pid                                           └┘                  └┘             
st                                         └─────────────────────┘└─────────────┘
 29    map_mul := λ x y, frobenius_inj α p _ _ (by simp only [frobenius_pth_root, frobenius_mul]),
id                     └───────────┘                      └────────────────┘  └───────────┘
src                      └───────────┘             └─────────┘└────────────────┘└┘└───────────┘
typ                    └───────────┘           └─────────┘└────────────────┘└┘└───────────┘
doc                                                └─────────┘                  └┘             
txt                                                └─────────┘                  └┘             
par                                                └─────────┘                  └┘             
pid                                                    └──┘└┘                  └┘             
st                                                └────────────────────────────────────────────┘
 30    map_add := λ x y, frobenius_inj α p _ _ (by simp only [frobenius_pth_root, frobenius_add]) }
id                     └───────────┘                      └────────────────┘  └───────────┘
src                      └───────────┘             └─────────┘└────────────────┘└┘└───────────┘
typ                    └───────────┘           └─────────┘└────────────────┘└┘└───────────┘
doc                                                └─────────┘                  └┘             
txt                                                └─────────┘                  └┘             
par                                                └─────────┘                  └┘             
pid                                                    └──┘└┘                  └┘             
st                                                └────────────────────────────────────────────┘
 31  
 32  theorem is_ring_hom.pth_root {α : Type u} [field α] (p : ℕ) [nat.prime p] [char_p α p] [perfect_field α p]
id                                              └───┘           └───────┘    └────┘     └───────────┘  
src                                             └───┘            └───────┘     └────┘       └───────────┘
typ                                             └───┘           └───────┘    └────┘     └───────────┘  
doc                                                               └───────┘     └────┘       └───────────┘
 33    {β : Type v} [field β] [char_p β p] [perfect_field β p] (f : α → β) [is_ring_hom f] {x : α} :
id                   └───┘    └────┘     └───────────┘               └─────────┘        
src                  └───┘     └────┘       └───────────┘                   └─────────┘
typ                  └───┘    └────┘     └───────────┘               └─────────┘        
doc                            └────┘       └───────────┘                   └─────────┘
 34    f (perfect_field.pth_root p x) = perfect_field.pth_root p (f x) :=
id       └────────────────────┘     └────────────────────┘    
src       └────────────────────┘       └────────────────────┘
typ      └────────────────────┘     └────────────────────┘    
 35  frobenius_inj β p _ _ (by rw [← is_monoid_hom.map_frobenius f, frobenius_pth_root, frobenius_pth_root])
id   └───────────┘                 └─────────────────────────┘   └────────────────┘  └────────────────┘
src  └───────────┘             └────┘└─────────────────────────┘ └┘└────────────────┘└┘└────────────────┘
typ  └───────────┘           └────┘└─────────────────────────┘└┘└────────────────┘└┘└────────────────┘
doc                            └────┘                            └┘                  └┘                  
txt                            └────┘                            └┘                  └┘                  
par                            └────┘                            └┘                  └┘                  
pid                              └──┘                            └┘                  └┘                  
st                            └──────────────────────────────────┘└──────────────────┘└──────────────────┘
 36  
 37  inductive perfect_closure.r (α : Type u) [monoid α] (p : ℕ) : (ℕ × α) → (ℕ × α) → Prop
id                                             └────┘                      
src                                            └────┘                       
typ                                            └────┘                      
 38  | intro : ∀ n x, perfect_closure.r (n, x) (n+1, frobenius α p x)
id                                           └───────┘     
src                                               └───────┘
typ                                          └───────┘     
doc                                                  └───────┘
 39  run_cmd tactic.mk_iff_of_inductive_prop `perfect_closure.r `perfect_closure.r_iff
id           └─────────────────────────────┘                   
src          └─────────────────────────────┘                   
typ          └─────────────────────────────┘                   
doc          └─────────────────────────────┘
 40  
 41  /-- The perfect closure is the smallest extension that makes frobenius surjective. -/
 42  def perfect_closure (α : Type u) [monoid α] (p : ℕ) : Type u :=
id                                     └────┘        
src                                    └────┘         
typ                                    └────┘        
 43  quot (perfect_closure.r α p)
id   └──┘  └───────────────┘  
src        └───────────────┘
typ  └──┘  └───────────────┘  
 44  
 45  namespace perfect_closure
 46  
 47  variables (α : Type u)
 48  
 49  private lemma mul_aux_left [comm_monoid α] (p : ℕ) (x1 x2 y : ℕ × α) (H : r α p x1 x2) :
id                               └─────────┘                                 └┘ └┘
src                              └─────────┘                                
typ                              └─────────┘                                 └┘ └┘
 50    quot.mk (r α p) (x1.1 + y.1, ((frobenius α p)^[y.1] x1.2) * ((frobenius α p)^[x1.1] y.2)) =
id     └─────┘      └┘        └───────┘   └┘  └┘      └───────┘   └┘└┘      
src                              └───────┘     └┘           └───────┘     └┘         
typ    └─────┘      └┘        └───────┘   └┘  └┘      └───────┘   └┘└┘      
doc                                   └───────┘                      └───────┘
 51    quot.mk (r α p) (x2.1 + y.1, ((frobenius α p)^[y.1] x2.2) * ((frobenius α p)^[x2.1] y.2)) :=
id     └─────┘      └┘        └───────┘   └┘  └┘      └───────┘   └┘└┘  
src                              └───────┘     └┘           └───────┘     └┘     
typ    └─────┘      └┘        └───────┘   └┘  └┘      └───────┘   └┘└┘  
doc                                   └───────┘                      └───────┘
 52  match x1, x2, H with
id         └┘  └┘  
typ        └┘  └┘  
 53  | _, _, r.intro _ n x := quot.sound $ by rw [← nat.iterate_succ, nat.iterate_succ',
id           └─────┘          └────────┘            └──────────────┘  └───────────────┘
src          └─────┘          └────────┘      └────┘└──────────────┘└┘└───────────────┘└─
typ          └─────┘          └────────┘      └────┘└──────────────┘└┘└───────────────┘└─
doc                                           └────┘                └┘                 └─
txt                                           └────┘                └┘                 └─
par                                           └────┘                └┘                 └─
pid                                             └──┘                └┘                 └─
st                                           └─────────────────────┘└─────────────────┘└─
 54      nat.iterate_succ', ← frobenius_mul, nat.succ_add]; apply r.intro
id       └───────────────┘    └───────────┘  └──────────┘         └─────┘
src  ───┘└───────────────┘└──┘└───────────┘└┘└──────────┘  └────┘└─────┘
typ  ───┘└───────────────┘└──┘└───────────┘└┘└──────────┘  └────┘└─────┘
doc  ───┘                 └──┘             └┘              └────┘       
txt  ───┘                 └──┘             └┘              └────┘       
par  ───┘                 └──┘             └┘              └────┘       
pid  ───┘                 └──┘             └┘                          
st   ────────────────────┘└───────────────┘└────────────┘└──────────────┘
 55  end
 56  
 57  private lemma mul_aux_right [comm_monoid α] (p : ℕ) (x y1 y2 : ℕ × α) (H : r α p y1 y2) :
id                                └─────────┘                                 └┘ └┘
src                               └─────────┘                                
typ                               └─────────┘                                 └┘ └┘
 58    quot.mk (r α p) (x.1 + y1.1, ((frobenius α p)^[y1.1] x.2) * ((frobenius α p)^[x.1] y1.2)) =
id     └─────┘         └┘     └───────┘   └┘└┘        └───────┘   └┘  └┘    
src                              └───────┘     └┘           └───────┘     └┘         
typ    └─────┘         └┘     └───────┘   └┘└┘        └───────┘   └┘  └┘    
doc                                   └───────┘                      └───────┘
 59    quot.mk (r α p) (x.1 + y2.1, ((frobenius α p)^[y2.1] x.2) * ((frobenius α p)^[x.1] y2.2)) :=
id     └─────┘         └┘     └───────┘   └┘└┘        └───────┘   └┘  └┘
src                              └───────┘     └┘           └───────┘     └┘     
typ    └─────┘         └┘     └───────┘   └┘└┘        └───────┘   └┘  └┘
doc                                   └───────┘                      └───────┘
 60  match y1, y2, H with
id         └┘  └┘  
typ        └┘  └┘  
 61  | _, _, r.intro _ n y := quot.sound $ by rw [← nat.iterate_succ, nat.iterate_succ',
id           └─────┘          └────────┘            └──────────────┘  └───────────────┘
src          └─────┘          └────────┘      └────┘└──────────────┘└┘└───────────────┘└─
typ          └─────┘          └────────┘      └────┘└──────────────┘└┘└───────────────┘└─
doc                                           └────┘                └┘                 └─
txt                                           └────┘                └┘                 └─
par                                           └────┘                └┘                 └─
pid                                             └──┘                └┘                 └─
st                                           └─────────────────────┘└─────────────────┘└─
 62      nat.iterate_succ', ← frobenius_mul]; apply r.intro
id       └───────────────┘    └───────────┘         └─────┘
src  ───┘└───────────────┘└──┘└───────────┘  └────┘└─────┘
typ  ───┘└───────────────┘└──┘└───────────┘  └────┘└─────┘
doc  ───┘                 └──┘               └────┘       
txt  ───┘                 └──┘               └────┘       
par  ───┘                 └──┘               └────┘       
pid  ───┘                 └──┘                           
st   ────────────────────┘└───────────────┘└──────────────┘
 63  end
 64  
 65  instance [comm_monoid α] (p : ℕ) : has_mul (perfect_closure α p) :=
id             └─────────┘            └─────┘  └─────────────┘  
src            └─────────┘             └─────┘  └─────────────┘
typ            └─────────┘            └─────┘  └─────────────┘  
doc                                              └─────────────┘
 66  ⟨quot.lift (λ x:ℕ×α, quot.lift (λ y:ℕ×α, quot.mk (r α p)
id    └───────┘        └───────┘        └─────┘    
src                                                
typ   └───────┘        └───────┘        └─────┘    
 67      (x.1 + y.1, ((frobenius α p)^[y.1] x.2) * ((frobenius α p)^[x.1] y.2))) (mul_aux_right α p x))
id               └───────┘   └┘        └───────┘   └┘        └───────────┘   
src                └───────┘     └┘          └───────┘     └┘          └───────────┘
typ              └───────┘   └┘        └───────┘   └┘        └───────────┘   
doc                    └───────┘                     └───────┘
 68    (λ x1 x2 (H : r α p x1 x2), funext $ λ e, quot.induction_on e $ λ y,
id        └┘ └┘         └┘ └┘   └────┘       └───────────────┘      
src                               └────┘        └───────────────┘
typ       └┘ └┘         └┘ └┘   └────┘       └───────────────┘      
 69  mul_aux_left α p x1 x2 y H)⟩
id   └──────────┘   └┘ └┘  
src  └──────────┘
typ  └──────────┘   └┘ └┘  
 70  
 71  instance [comm_monoid α] (p : ℕ) : comm_monoid (perfect_closure α p) :=
id             └─────────┘            └─────────┘  └─────────────┘  
src            └─────────┘             └─────────┘  └─────────────┘
typ            └─────────┘            └─────────┘  └─────────────┘  
doc                                                  └─────────────┘
 72  { mul_assoc := λ e f g, quot.induction_on e $ λ ⟨m, x⟩, quot.induction_on f $ λ ⟨n, y⟩,
id                        └───────────────┘             └───────────────┘      
src                          └───────────────┘               └───────────────┘
typ                       └───────────────┘             └───────────────┘      
 73      quot.induction_on g $ λ ⟨s, z⟩, congr_arg (quot.mk _) $
id       └───────────────┘             └───────┘  └─────┘
src      └───────────────┘               └───────┘
typ      └───────────────┘             └───────┘  └─────┘
 74      by simp only [add_assoc, mul_assoc, nat.iterate₂ (frobenius_mul _ _),
id                     └───────┘  └───────┘  └──────────┘  └───────────┘
src         └─────────┘└───────┘└┘└───────┘└┘└──────────┘ └───────────┘└──────
typ         └─────────┘└───────┘└┘└───────┘└┘└──────────┘ └───────────┘└──────
doc         └─────────┘         └┘         └┘                          └──────
txt         └─────────┘         └┘         └┘                          └──────
par         └─────────┘         └┘         └┘                          └──────
pid             └──┘└┘         └┘         └┘                          └──────
st         └───────────────────────────────────────────────────────────────────
 75        (nat.iterate_add _ _ _ _).symm, add_comm, add_left_comm],
id          └─────────────┘                └──────┘  └───────────┘
src  ─────┘ └─────────────┘└──────────────┘└──────┘└┘└───────────┘
typ  ─────┘ └─────────────┘└──────────────┘└──────┘└┘└───────────┘
doc  ─────┘                └──────────────┘        └┘             
txt  ─────┘                └──────────────┘        └┘             
par  ─────┘                └──────────────┘        └┘             
pid  ─────┘                └──────────────┘        └┘             
st   ─────────────────────────────────────────────────────────────┘
 76    one := quot.mk _ (0, 1),
id            └─────┘   
src                     
typ           └─────┘   
 77    one_mul := λ e, quot.induction_on e (λ ⟨n, x⟩, congr_arg (quot.mk _) $
id                    └───────────────┘            └───────┘  └─────┘
src                    └───────────────┘              └───────┘
typ                   └───────────────┘            └───────┘  └─────┘
 78      by simp only [nat.iterate₀ (frobenius_one _ _), nat.iterate_zero, one_mul, zero_add]),
id                     └──────────┘  └───────────┘       └──────────────┘  └─────┘  └──────┘
src         └─────────┘└──────────┘ └───────────┘└─────┘└──────────────┘└┘└─────┘└┘└──────┘
typ         └─────────┘└──────────┘ └───────────┘└─────┘└──────────────┘└┘└─────┘└┘└──────┘
doc         └─────────┘                          └─────┘                └┘       └┘        
txt         └─────────┘                          └─────┘                └┘       └┘        
par         └─────────┘                          └─────┘                └┘       └┘        
pid             └──┘└┘                          └─────┘                └┘       └┘        
st         └────────────────────────────────────────────────────────────────────────────────┘
 79    mul_one := λ e, quot.induction_on e (λ ⟨n, x⟩, congr_arg (quot.mk _) $
id                    └───────────────┘            └───────┘  └─────┘
src                    └───────────────┘              └───────┘
typ                   └───────────────┘            └───────┘  └─────┘
 80      by simp only [nat.iterate₀ (frobenius_one _ _), nat.iterate_zero, mul_one, add_zero]),
id                     └──────────┘  └───────────┘       └──────────────┘  └─────┘  └──────┘
src         └─────────┘└──────────┘ └───────────┘└─────┘└──────────────┘└┘└─────┘└┘└──────┘
typ         └─────────┘└──────────┘ └───────────┘└─────┘└──────────────┘└┘└─────┘└┘└──────┘
doc         └─────────┘                          └─────┘                └┘       └┘        
txt         └─────────┘                          └─────┘                └┘       └┘        
par         └─────────┘                          └─────┘                └┘       └┘        
pid             └──┘└┘                          └─────┘                └┘       └┘        
st         └────────────────────────────────────────────────────────────────────────────────┘
 81    mul_comm := λ e f, quot.induction_on e (λ ⟨m, x⟩, quot.induction_on f (λ ⟨n, y⟩,
id                      └───────────────┘            └───────────────┘     
src                       └───────────────┘              └───────────────┘
typ                     └───────────────┘            └───────────────┘     
 82      congr_arg (quot.mk _) $ by simp only [add_comm, mul_comm])),
id       └───────┘  └─────┘                    └──────┘  └──────┘
src      └───────┘                  └─────────┘└──────┘└┘└──────┘
typ      └───────┘  └─────┘         └─────────┘└──────┘└┘└──────┘
doc                                 └─────────┘        └┘        
txt                                 └─────────┘        └┘        
par                                 └─────────┘        └┘        
pid                                     └──┘└┘        └┘        
st                                 └─────────────────────────────┘
 83    .. (infer_instance : has_mul (perfect_closure α p)) }
id         └────────────┘   └─────┘  └─────────────┘  
src        └────────────┘   └─────┘  └─────────────┘
typ        └────────────┘   └─────┘  └─────────────┘  
doc        └────────────┘            └─────────────┘
 84  
 85  instance [comm_monoid α] (p) : inhabited (perfect_closure α p) := ⟨1⟩
id             └─────────┘         └───────┘  └─────────────┘  
src            └─────────┘          └───────┘  └─────────────┘
typ            └─────────┘         └───────┘  └─────────────┘  
doc                                            └─────────────┘
 86  
 87  private lemma add_aux_left [comm_ring α] (p : ℕ) (hp : nat.prime p) [char_p α p]
id                               └───────┘                └───────┘    └────┘  
src                              └───────┘                 └───────┘     └────┘
typ                              └───────┘                └───────┘    └────┘  
doc                                                         └───────┘     └────┘
 88    (x1 x2 y : ℕ × α) (H : r α p x1 x2) :
id                            └┘ └┘
src                         
typ                           └┘ └┘
 89    quot.mk (r α p) (x1.1 + y.1, ((frobenius α p)^[y.1] x1.2) + ((frobenius α p)^[x1.1] y.2)) =
id     └─────┘      └┘        └───────┘   └┘  └┘      └───────┘   └┘└┘      
src                              └───────┘     └┘           └───────┘     └┘         
typ    └─────┘      └┘        └───────┘   └┘  └┘      └───────┘   └┘└┘      
doc                                   └───────┘                      └───────┘
 90    quot.mk (r α p) (x2.1 + y.1, ((frobenius α p)^[y.1] x2.2) + ((frobenius α p)^[x2.1] y.2)) :=
id     └─────┘      └┘        └───────┘   └┘  └┘      └───────┘   └┘└┘  
src                              └───────┘     └┘           └───────┘     └┘     
typ    └─────┘      └┘        └───────┘   └┘  └┘      └───────┘   └┘└┘  
doc                                   └───────┘                      └───────┘
 91  match x1, x2, H with
id         └┘  └┘  
typ        └┘  └┘  
 92  | _, _, r.intro _ n x := quot.sound $ by rw [← nat.iterate_succ, nat.iterate_succ',
id           └─────┘          └────────┘            └──────────────┘  └───────────────┘
src          └─────┘          └────────┘      └────┘└──────────────┘└┘└───────────────┘└─
typ          └─────┘          └────────┘      └────┘└──────────────┘└┘└───────────────┘└─
doc                                           └────┘                └┘                 └─
txt                                           └────┘                └┘                 └─
par                                           └────┘                └┘                 └─
pid                                             └──┘                └┘                 └─
st                                           └─────────────────────┘└─────────────────┘└─
 93      nat.iterate_succ', ← frobenius_add, nat.succ_add]; apply r.intro
id       └───────────────┘    └───────────┘  └──────────┘         └─────┘
src  ───┘└───────────────┘└──┘└───────────┘└┘└──────────┘  └────┘└─────┘
typ  ───┘└───────────────┘└──┘└───────────┘└┘└──────────┘  └────┘└─────┘
doc  ───┘                 └──┘             └┘              └────┘       
txt  ───┘                 └──┘             └┘              └────┘       
par  ───┘                 └──┘             └┘              └────┘       
pid  ───┘                 └──┘             └┘                          
st   ────────────────────┘└───────────────┘└────────────┘└──────────────┘
 94  end
 95  
 96  private lemma add_aux_right [comm_ring α] (p : ℕ) (hp : nat.prime p) [char_p α p]
id                                └───────┘                └───────┘    └────┘  
src                               └───────┘                 └───────┘     └────┘
typ                               └───────┘                └───────┘    └────┘  
doc                                                          └───────┘     └────┘
 97    (x y1 y2 : ℕ × α) (H : r α p y1 y2) :
id                            └┘ └┘
src                         
typ                           └┘ └┘
 98    quot.mk (r α p) (x.1 + y1.1, ((frobenius α p)^[y1.1] x.2) + ((frobenius α p)^[x.1] y1.2)) =
id     └─────┘         └┘     └───────┘   └┘└┘        └───────┘   └┘  └┘    
src                              └───────┘     └┘           └───────┘     └┘         
typ    └─────┘         └┘     └───────┘   └┘└┘        └───────┘   └┘  └┘    
doc                                   └───────┘                      └───────┘
 99    quot.mk (r α p) (x.1 + y2.1, ((frobenius α p)^[y2.1] x.2) + ((frobenius α p)^[x.1] y2.2)) :=
id     └─────┘         └┘     └───────┘   └┘└┘        └───────┘   └┘  └┘
src                              └───────┘     └┘           └───────┘     └┘     
typ    └─────┘         └┘     └───────┘   └┘└┘        └───────┘   └┘  └┘
doc                                   └───────┘                      └───────┘
100  match y1, y2, H with
id         └┘  └┘  
typ        └┘  └┘  
101  | _, _, r.intro _ n y := quot.sound $ by rw [← nat.iterate_succ, nat.iterate_succ',
id           └─────┘          └────────┘            └──────────────┘  └───────────────┘
src          └─────┘          └────────┘      └────┘└──────────────┘└┘└───────────────┘└─
typ          └─────┘          └────────┘      └────┘└──────────────┘└┘└───────────────┘└─
doc                                           └────┘                └┘                 └─
txt                                           └────┘                └┘                 └─
par                                           └────┘                └┘                 └─
pid                                             └──┘                └┘                 └─
st                                           └─────────────────────┘└─────────────────┘└─
102      nat.iterate_succ', ← frobenius_add]; apply r.intro
id       └───────────────┘    └───────────┘         └─────┘
src  ───┘└───────────────┘└──┘└───────────┘  └────┘└─────┘
typ  ───┘└───────────────┘└──┘└───────────┘  └────┘└─────┘
doc  ───┘                 └──┘               └────┘       
txt  ───┘                 └──┘               └────┘       
par  ───┘                 └──┘               └────┘       
pid  ───┘                 └──┘                           
st   ────────────────────┘└───────────────┘└──────────────┘
103  end
104  
105  instance [comm_ring α] (p : ℕ) [hp : nat.prime p] [char_p α p] : has_add (perfect_closure α p) :=
id             └───────┘                └───────┘    └────┘      └─────┘  └─────────────┘  
src            └───────┘                 └───────┘     └────┘        └─────┘  └─────────────┘
typ            └───────┘                └───────┘    └────┘      └─────┘  └─────────────┘  
doc                                       └───────┘     └────┘                 └─────────────┘
106  ⟨quot.lift (λ x:ℕ×α, quot.lift (λ y:ℕ×α, quot.mk (r α p)
id    └───────┘        └───────┘        └─────┘    
src                                                
typ   └───────┘        └───────┘        └─────┘    
107      (x.1 + y.1, ((frobenius α p)^[y.1] x.2) + ((frobenius α p)^[x.1] y.2))) (add_aux_right α p hp x))
id               └───────┘   └┘        └───────┘   └┘        └───────────┘   └┘ 
src                └───────┘     └┘          └───────┘     └┘          └───────────┘
typ              └───────┘   └┘        └───────┘   └┘        └───────────┘   └┘ 
doc                    └───────┘                     └───────┘
108    (λ x1 x2 (H : r α p x1 x2), funext $ λ e, quot.induction_on e $ λ y,
id        └┘ └┘         └┘ └┘   └────┘       └───────────────┘      
src                               └────┘        └───────────────┘
typ       └┘ └┘         └┘ └┘   └────┘       └───────────────┘      
109  add_aux_left α p hp x1 x2 y H)⟩
id   └──────────┘   └┘ └┘ └┘  
src  └──────────┘
typ  └──────────┘   └┘ └┘ └┘  
110  
111  instance [comm_ring α] (p : ℕ) [nat.prime p] [char_p α p] : has_neg (perfect_closure α p) :=
id             └───────┘           └───────┘    └────┘      └─────┘  └─────────────┘  
src            └───────┘            └───────┘     └────┘        └─────┘  └─────────────┘
typ            └───────┘           └───────┘    └────┘      └─────┘  └─────────────┘  
doc                                  └───────┘     └────┘                 └─────────────┘
112  ⟨quot.lift (λ x:ℕ×α, quot.mk (r α p) (x.1, -x.2)) (λ x y (H : r α p x y), match x, y, H with
id    └───────┘        └─────┘                                        
src                                                         
typ   └───────┘        └─────┘                                        
113  | _, _, r.intro _ n x := quot.sound $ by rw ← frobenius_neg; apply r.intro
id           └─────┘          └────────┘           └───────────┘        └─────┘
src          └─────┘          └────────┘      └───┘└───────────┘  └────┘└─────┘
typ          └─────┘          └────────┘      └───┘└───────────┘  └────┘└─────┘
doc                                           └───┘               └────┘       
txt                                           └───┘               └────┘       
par                                           └───┘               └────┘       
pid                                             └─┘                           
st                                           └─────────────────────────────────┘
114  end)⟩
115  
116  theorem mk_zero [comm_ring α] (p : ℕ) [nat.prime p] (n : ℕ) : quot.mk (r α p) (n, 0) = quot.mk (r α p) (0, 0) :=
id                    └───────┘           └───────┘            └─────┘            └─────┘      
src                   └───────┘            └───────┘                                                  
typ                   └───────┘           └───────┘            └─────┘            └─────┘      
doc                                         └───────┘
117  by induction n with n ih; [refl, rw ← ih]; symmetry; apply quot.sound;
id                                       └┘                   └────────┘
src     └────────┘ └────────┘  └──┘  └───┘     └──────┘  └────┘└────────┘
typ     └────────┘└────────┘  └──┘  └───┘└┘   └──────┘  └────┘└────────┘
doc     └────────┘ └────────┘   └──┘  └───┘     └──────┘  └────┘
txt     └────────┘ └────────┘   └──┘  └───┘     └──────┘  └────┘
par     └────────┘ └────────┘   └──┘  └───┘     └──────┘  └────┘
pid               └───────┘           └─┘                    
st     └────────────────────────────────────────────────────────────────────
118  have := r.intro p n (0:α); rwa [frobenius_zero α p] at this
id           └─────┘              └────────────┘  
src  └──────┘└─────┘   └┘   └───┘└────────────┘  └─────────
typ  └──────┘└─────┘ └┘  └───┘└────────────┘└─────────
doc  └──────┘          └┘   └───┘                └─────────
txt  └──────┘          └┘   └───┘                └─────────
par  └──────┘          └┘   └───┘                └─────────
pid  └───┘└─┘          └┘      └┘                └──────┘
st   ───────────────────────────────┘└────────────────┘└────────
119  
src  
typ  
doc  
txt  
par  
pid  
st   
120  theorem r.sound [monoid α] (p m n : ℕ) (x y : α) (H : frobenius α p^[m] x = y) :
id                    └────┘                            └───────┘  └┘   
src                   └────┘                              └───────┘    └┘    
typ                   └────┘                            └───────┘  └┘   
doc                                                        └───────┘
121    quot.mk (r α p) (n, x) = quot.mk (r α p) (m + n, y) :=
id     └─────┘           └─────┘          
src                                           
typ    └─────┘           └─────┘          
122  by subst H; induction m with m ih; [simp only [zero_add, nat.iterate_zero],
id                                               └──────┘  └──────────────┘
src     └────┘   └────────┘ └────────┘  └─────────┘└──────┘└┘└──────────────┘
typ     └────┘  └────────┘└────────┘  └─────────┘└──────┘└┘└──────────────┘
doc     └────┘   └────────┘ └────────┘   └─────────┘        └┘                
txt     └────┘   └────────┘ └────────┘   └─────────┘        └┘                
par     └────┘   └────────┘ └────────┘   └─────────┘        └┘                
pid                       └───────┘       └──┘└┘        └┘                
st     └─────────────────────────────────────────────────────────────────────────
123    rw [ih, nat.succ_add, nat.iterate_succ']]; apply quot.sound; apply r.intro
id         └┘  └──────────┘  └───────────────┘          └────────┘        └─────┘
src    └──┘  └┘└──────────┘└┘└───────────────┘   └────┘└────────┘  └────┘└─────┘
typ    └──┘└┘└┘└──────────┘└┘└───────────────┘   └────┘└────────┘  └────┘└─────┘
doc    └──┘  └┘            └┘                    └────┘            └────┘       
txt    └──┘  └┘            └┘                    └────┘            └────┘       
par    └──┘  └┘            └┘                    └────┘            └────┘       
pid      └┘  └┘            └┘                                                 
st   ─────┘└┘└────────────┘└─────────────────┘└──────────────────────────────────
124  
src  
typ  
doc  
txt  
par  
pid  
st   
125  instance [comm_ring α] (p : ℕ) [nat.prime p] [char_p α p] : comm_ring (perfect_closure α p) :=
id             └───────┘           └───────┘    └────┘      └───────┘  └─────────────┘  
src            └───────┘            └───────┘     └────┘        └───────┘  └─────────────┘
typ            └───────┘           └───────┘    └────┘      └───────┘  └─────────────┘  
doc                                  └───────┘     └────┘                   └─────────────┘
126  { add_assoc := λ e f g, quot.induction_on e $ λ ⟨m, x⟩, quot.induction_on f $ λ ⟨n, y⟩,
id                        └───────────────┘             └───────────────┘      
src                          └───────────────┘               └───────────────┘
typ                       └───────────────┘             └───────────────┘      
127      quot.induction_on g $ λ ⟨s, z⟩, congr_arg (quot.mk _) $
id       └───────────────┘             └───────┘  └─────┘
src      └───────────────┘               └───────┘
typ      └───────────────┘             └───────┘  └─────┘
128      by simp only [add_assoc, nat.iterate₂ (frobenius_add α p),
id                     └───────┘  └──────────┘  └───────────┘  
src         └─────────┘└───────┘└┘└──────────┘ └───────────┘  └──
typ         └─────────┘└───────┘└┘└──────────┘ └───────────┘└──
doc         └─────────┘         └┘                            └──
txt         └─────────┘         └┘                            └──
par         └─────────┘         └┘                            └──
pid             └──┘└┘         └┘                            └──
st         └────────────────────────────────────────────────────────
129        (nat.iterate_add _ _ _ _).symm, add_comm, add_left_comm],
id          └─────────────┘                └──────┘  └───────────┘
src  ─────┘ └─────────────┘└──────────────┘└──────┘└┘└───────────┘
typ  ─────┘ └─────────────┘└──────────────┘└──────┘└┘└───────────┘
doc  ─────┘                └──────────────┘        └┘             
txt  ─────┘                └──────────────┘        └┘             
par  ─────┘                └──────────────┘        └┘             
pid  ─────┘                └──────────────┘        └┘             
st   ─────────────────────────────────────────────────────────────┘
130    zero := quot.mk _ (0, 0),
id             └─────┘   
src                      
typ            └─────┘   
131    zero_add := λ e, quot.induction_on e (λ ⟨n, x⟩, congr_arg (quot.mk _) $
id                     └───────────────┘            └───────┘  └─────┘
src                     └───────────────┘              └───────┘
typ                    └───────────────┘            └───────┘  └─────┘
132      by simp only [nat.iterate₀ (frobenius_zero α p), nat.iterate_zero, zero_add]),
id                     └──────────┘  └────────────┘     └──────────────┘  └──────┘
src         └─────────┘└──────────┘ └────────────┘  └─┘└──────────────┘└┘└──────┘
typ         └─────────┘└──────────┘ └────────────┘└─┘└──────────────┘└┘└──────┘
doc         └─────────┘                             └─┘                └┘        
txt         └─────────┘                             └─┘                └┘        
par         └─────────┘                             └─┘                └┘        
pid             └──┘└┘                             └─┘                └┘        
st         └────────────────────────────────────────────────────────────────────────┘
133    add_zero := λ e, quot.induction_on e (λ ⟨n, x⟩, congr_arg (quot.mk _) $
id                     └───────────────┘            └───────┘  └─────┘
src                     └───────────────┘              └───────┘
typ                    └───────────────┘            └───────┘  └─────┘
134      by simp only [nat.iterate₀ (frobenius_zero α p), nat.iterate_zero, add_zero]),
id                     └──────────┘  └────────────┘     └──────────────┘  └──────┘
src         └─────────┘└──────────┘ └────────────┘  └─┘└──────────────┘└┘└──────┘
typ         └─────────┘└──────────┘ └────────────┘└─┘└──────────────┘└┘└──────┘
doc         └─────────┘                             └─┘                └┘        
txt         └─────────┘                             └─┘                └┘        
par         └─────────┘                             └─┘                └┘        
pid             └──┘└┘                             └─┘                └┘        
st         └────────────────────────────────────────────────────────────────────────┘
135    add_left_neg := λ e, quot.induction_on e (λ ⟨n, x⟩, show quot.mk _ _ = _,
id                         └───────────────┘                 └─────┘     
src                         └───────────────┘                               
typ                        └───────────────┘                 └─────┘     
136      by simp only [nat.iterate₁ (frobenius_neg α p), add_left_neg, mk_zero]; refl),
id                     └──────────┘  └───────────┘     └──────────┘  └─────┘
src         └─────────┘└──────────┘ └───────────┘  └─┘└──────────┘└┘└─────┘  └──┘
typ         └─────────┘└──────────┘ └───────────┘└─┘└──────────┘└┘└─────┘  └──┘
doc         └─────────┘                            └─┘            └┘         └──┘
txt         └─────────┘                            └─┘            └┘         └──┘
par         └─────────┘                            └─┘            └┘         └──┘
pid             └──┘└┘                            └─┘            └┘       
st         └────────────────────────────────────────────────────────────────────────┘
137    add_comm := λ e f, quot.induction_on e (λ ⟨m, x⟩, quot.induction_on f (λ ⟨n, y⟩,
id                      └───────────────┘            └───────────────┘     
src                       └───────────────┘              └───────────────┘
typ                     └───────────────┘            └───────────────┘     
138      congr_arg (quot.mk _) $ by simp only [add_comm])),
id       └───────┘  └─────┘                    └──────┘
src      └───────┘                  └─────────┘└──────┘
typ      └───────┘  └─────┘         └─────────┘└──────┘
doc                                 └─────────┘        
txt                                 └─────────┘        
par                                 └─────────┘        
pid                                     └──┘└┘        
st                                 └───────────────────┘
139    left_distrib := λ e f g, quot.induction_on e $ λ ⟨m, x⟩, quot.induction_on f $ λ ⟨n, y⟩,
id                           └───────────────┘             └───────────────┘      
src                             └───────────────┘               └───────────────┘
typ                          └───────────────┘             └───────────────┘      
140      quot.induction_on g $ λ ⟨s, z⟩, show quot.mk _ _ = quot.mk _ _,
id       └───────────────┘                  └─────┘      └─────┘
src      └───────────────┘                                
typ      └───────────────┘                  └─────┘      └─────┘
141      by simp only [add_assoc, add_comm, add_left_comm]; apply r.sound;
id                     └───────┘  └──────┘  └───────────┘         └─────┘
src         └─────────┘└───────┘└┘└──────┘└┘└───────────┘  └────┘└─────┘
typ         └─────────┘└───────┘└┘└──────┘└┘└───────────┘  └────┘└─────┘
doc         └─────────┘         └┘        └┘               └────┘
txt         └─────────┘         └┘        └┘               └────┘
par         └─────────┘         └┘        └┘               └────┘
pid             └──┘└┘         └┘        └┘                    
st         └───────────────────────────────────────────────────────────────
142      simp only [nat.iterate₂ (frobenius_mul α p), nat.iterate₂ (frobenius_add α p),
id                  └──────────┘  └───────────┘     └──────────┘  └───────────┘  
src      └─────────┘└──────────┘ └───────────┘  └─┘└──────────┘ └───────────┘  └──
typ      └─────────┘└──────────┘ └───────────┘└─┘└──────────┘ └───────────┘└──
doc      └─────────┘                            └─┘                            └──
txt      └─────────┘                            └─┘                            └──
par      └─────────┘                            └─┘                            └──
pid          └──┘└┘                            └─┘                            └──
st   ───────────────────────────────────────────────────────────────────────────────────
143        (nat.iterate_add _ _ _ _).symm, mul_add, add_comm, add_left_comm],
id          └─────────────┘                └─────┘  └──────┘  └───────────┘
src  ─────┘ └─────────────┘└──────────────┘└─────┘└┘└──────┘└┘└───────────┘
typ  ─────┘ └─────────────┘└──────────────┘└─────┘└┘└──────┘└┘└───────────┘
doc  ─────┘                └──────────────┘       └┘        └┘             
txt  ─────┘                └──────────────┘       └┘        └┘             
par  ─────┘                └──────────────┘       └┘        └┘             
pid  ─────┘                └──────────────┘       └┘        └┘             
st   ──────────────────────────────────────────────────────────────────────┘
144    right_distrib := λ e f g, quot.induction_on e $ λ ⟨m, x⟩, quot.induction_on f $ λ ⟨n, y⟩,
id                            └───────────────┘             └───────────────┘      
src                              └───────────────┘               └───────────────┘
typ                           └───────────────┘             └───────────────┘      
145      quot.induction_on g $ λ ⟨s, z⟩, show quot.mk _ _ = quot.mk _ _,
id       └───────────────┘                  └─────┘      └─────┘
src      └───────────────┘                                
typ      └───────────────┘                  └─────┘      └─────┘
146      by simp only [add_assoc, add_comm _ s, add_left_comm _ s]; apply r.sound;
id                     └───────┘  └──────┘     └───────────┘            └─────┘
src         └─────────┘└───────┘└┘└──────┘└─┘ └┘└───────────┘└─┘   └────┘└─────┘
typ         └─────────┘└───────┘└┘└──────┘└─┘└┘└───────────┘└─┘  └────┘└─────┘
doc         └─────────┘         └┘        └─┘ └┘             └─┘   └────┘
txt         └─────────┘         └┘        └─┘ └┘             └─┘   └────┘
par         └─────────┘         └┘        └─┘ └┘             └─┘   └────┘
pid             └──┘└┘         └┘        └─┘ └┘             └─┘        
st         └───────────────────────────────────────────────────────────────────────
147      simp only [nat.iterate₂ (frobenius_mul α p), nat.iterate₂ (frobenius_add α p),
id                  └──────────┘  └───────────┘     └──────────┘  └───────────┘  
src      └─────────┘└──────────┘ └───────────┘  └─┘└──────────┘ └───────────┘  └──
typ      └─────────┘└──────────┘ └───────────┘└─┘└──────────┘ └───────────┘└──
doc      └─────────┘                            └─┘                            └──
txt      └─────────┘                            └─┘                            └──
par      └─────────┘                            └─┘                            └──
pid          └──┘└┘                            └─┘                            └──
st   ───────────────────────────────────────────────────────────────────────────────────
148        (nat.iterate_add _ _ _ _).symm, add_mul, add_comm, add_left_comm],
id          └─────────────┘                └─────┘  └──────┘  └───────────┘
src  ─────┘ └─────────────┘└──────────────┘└─────┘└┘└──────┘└┘└───────────┘
typ  ─────┘ └─────────────┘└──────────────┘└─────┘└┘└──────┘└┘└───────────┘
doc  ─────┘                └──────────────┘       └┘        └┘             
txt  ─────┘                └──────────────┘       └┘        └┘             
par  ─────┘                └──────────────┘       └┘        └┘             
pid  ─────┘                └──────────────┘       └┘        └┘             
st   ──────────────────────────────────────────────────────────────────────┘
149    .. (infer_instance : has_add (perfect_closure α p)),
id         └────────────┘   └─────┘  └─────────────┘  
src        └────────────┘   └─────┘  └─────────────┘
typ        └────────────┘   └─────┘  └─────────────┘  
doc        └────────────┘            └─────────────┘
150    .. (infer_instance : has_neg (perfect_closure α p)),
id         └────────────┘   └─────┘  └─────────────┘  
src        └────────────┘   └─────┘  └─────────────┘
typ        └────────────┘   └─────┘  └─────────────┘  
doc        └────────────┘            └─────────────┘
151    .. (infer_instance : comm_monoid (perfect_closure α p)) }
id         └────────────┘   └─────────┘  └─────────────┘  
src        └────────────┘   └─────────┘  └─────────────┘
typ        └────────────┘   └─────────┘  └─────────────┘  
doc        └────────────┘                └─────────────┘
152  
153  instance [discrete_field α] (p : ℕ) [nat.prime p] [char_p α p] : has_inv (perfect_closure α p) :=
id             └────────────┘           └───────┘    └────┘      └─────┘  └─────────────┘  
src            └────────────┘            └───────┘     └────┘        └─────┘  └─────────────┘
typ            └────────────┘           └───────┘    └────┘      └─────┘  └─────────────┘  
doc                                       └───────┘     └────┘                 └─────────────┘
154  ⟨quot.lift (λ x:ℕ×α, quot.mk (r α p) (x.1, x.2⁻¹)) (λ x y (H : r α p x y), match x, y, H with
id    └───────┘        └─────┘          └┘                              
src                                          └┘               
typ   └───────┘        └─────┘          └┘                              
155  | _, _, r.intro _ n x := quot.sound $ by simp only [frobenius]; rw ← inv_pow'; apply r.intro
id           └─────┘          └────────┘                 └───────┘        └──────┘        └─────┘
src          └─────┘          └────────┘      └─────────┘└───────┘  └───┘└──────┘  └────┘└─────┘
typ          └─────┘          └────────┘      └─────────┘└───────┘  └───┘└──────┘  └────┘└─────┘
doc                                           └─────────┘└───────┘  └───┘          └────┘       
txt                                           └─────────┘           └───┘          └────┘       
par                                           └─────────┘           └───┘          └────┘       
pid                                               └──┘└┘             └─┘                      
st                                           └───────────────────────────────────────────────────┘
156  end)⟩
157  
158  theorem eq_iff' [comm_ring α] (p : ℕ) [nat.prime p] [char_p α p]
id                    └───────┘           └───────┘    └────┘  
src                   └───────┘            └───────┘     └────┘
typ                   └───────┘           └───────┘    └────┘  
doc                                         └───────┘     └────┘
159    (x y : ℕ × α) : quot.mk (r α p) x = quot.mk (r α p) y ↔
id                  └─────┘        └─────┘       
src                                                     
typ                 └─────┘        └─────┘       
160      ∃ z, (frobenius α p^[y.1 + z] x.2) = (frobenius α p^[x.1 + z] y.2) :=
id          └───────┘  └┘         └───────┘  └┘    
src          └───────┘    └┘            └───────┘    └┘       
typ         └───────┘  └┘         └───────┘  └┘    
doc            └───────┘                       └───────┘
161  begin
st   └─────
162    split,
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
st   ──────┘└─
163    { intro H,
src      └─────┘
typ      └─────┘
doc      └─────┘
txt      └─────┘
par      └─────┘
pid           └┘
st   ───┘└─────┘└─
164      replace H := quot.exact _ H,
id                    └────────┘   
src      └───────────┘└────────┘└─┘
typ      └───────────┘└────────┘└─┘
doc      └───────────┘          └─┘
txt      └───────────┘          └─┘
par      └───────────┘          └─┘
pid             └┘└─┘          └─┘
st   ──────────────────────────────┘└─
165      induction H,
id                 
src      └────────┘
typ      └────────┘
doc      └────────┘
txt      └────────┘
par      └────────┘
pid               
st   ──────────────┘└─
166      case eqv_gen.rel : x y H
src      └────────────────────────
typ      └────────────────────────
doc      └────────────────────────
txt      └────────────────────────
par      └────────────────────────
pid          └──────────┘└──────┘
st   ─────────────────────────────
167      { cases H with n x, exact ⟨0, rfl⟩ },
id                                    └─┘
src  ─────┘└────┘ └───────┘└┘└────┘ └─┘└─┘└┘
typ  ─────┘└────┘└───────┘└┘└────┘ └─┘└─┘└┘
doc  ─────┘└────┘ └───────┘└┘└────┘ └─┘   └┘
txt  ─────┘└────┘ └───────┘└┘└────┘ └─┘   └┘
par  ─────┘└────┘ └───────┘└┘└────┘ └─┘   └┘
pid  ───────────┘ └───────────────┘ └─┘   └─┘
st   ────┘└───────────────┘└───────────────┘└┘
168      case eqv_gen.refl : H
src      └─────────────────────
typ      └─────────────────────
doc      └─────────────────────
txt      └─────────────────────
par      └─────────────────────
pid          └───────────┘└──┘
st   ──────────────────────────
169      { exact ⟨0, rfl⟩ },
id                   └─┘
src  ─────┘└────┘ └─┘└─┘└┘
typ  ─────┘└────┘ └─┘└─┘└┘
doc  ─────┘└────┘ └─┘   └┘
txt  ─────┘└────┘ └─┘   └┘
par  ─────┘└────┘ └─┘   └┘
pid  ───────────┘ └─┘   └─┘
st   ────┘└──────────────┘└┘
170      case eqv_gen.symm : x y H ih
src      └────────────────────────────
typ      └────────────────────────────
doc      └────────────────────────────
txt      └────────────────────────────
par      └────────────────────────────
pid          └───────────┘└─────────┘
st   ─────────────────────────────────
171      { cases ih with w ih, exact ⟨w, ih.symm⟩ },
id               └┘                     └─────┘
src  ─────┘└────┘  └────────┘└┘└────┘  └┘└─────┘└┘
typ  ─────┘└────┘└┘└────────┘└┘└────┘ └┘└─────┘└┘
doc  ─────┘└────┘  └────────┘└┘└────┘  └┘       └┘
txt  ─────┘└────┘  └────────┘└┘└────┘  └┘       └┘
par  ─────┘└────┘  └────────┘└┘└────┘  └┘       └┘
pid  ───────────┘  └────────────────┘  └┘       └─┘
st   ────┘└─────────────────┘└───────────────────┘└┘
172      case eqv_gen.trans : x y z H1 H2 ih1 ih2
src      └────────────────────────────────────────
typ      └────────────────────────────────────────
doc      └────────────────────────────────────────
txt      └────────────────────────────────────────
par      └────────────────────────────────────────
pid          └────────────┘└────────────────────┘
st   ─────────────────────────────────────────────
173      { cases ih1 with z1 ih1,
id               └─┘
src  ─────┘└────┘   └──────────┘└─
typ  ─────┘└────┘└─┘└──────────┘└─
doc  ─────┘└────┘   └──────────┘└─
txt  ─────┘└────┘   └──────────┘└─
par  ─────┘└────┘   └──────────┘└─
pid  ───────────┘   └─────────────
st   ────┘└────────────────────┘└─
174        cases ih2 with z2 ih2,
id               └─┘
src  ─────┘└────┘   └──────────┘└─
typ  ─────┘└────┘└─┘└──────────┘└─
doc  ─────┘└────┘   └──────────┘└─
txt  ─────┘└────┘   └──────────┘└─
par  ─────┘└────┘   └──────────┘└─
pid  ───────────┘   └─────────────
st   ──────────────────────────┘└─
175        existsi z2+(y.1+z1),
id                 └┘    └┘
src  ─────┘└──────┘    └┘   └─
typ  ─────┘└──────┘└┘ └┘ └┘└─
doc  ─────┘└──────┘     └┘   └─
txt  ─────┘└──────┘     └┘   └─
par  ─────┘└──────┘     └┘   └─
pid  ─────────────┘     └┘   └──
st   ────────────────────────┘└─
176        rw [← add_assoc, nat.iterate_add, ih1],
id               └───────┘  └─────────────┘  └─┘
src  ─────┘└────┘└───────┘└┘└─────────────┘└┘   └─
typ  ─────┘└────┘└───────┘└┘└─────────────┘└┘└─┘└─
doc  ─────┘└────┘         └┘               └┘   └─
txt  ─────┘└────┘         └┘               └┘   └─
par  ─────┘└────┘         └┘               └┘   └─
pid  ───────────┘         └┘               └┘   └──
st   ────────────────────┘└───────────────┘└───┘└──
177        rw [← nat.iterate_add, add_comm, nat.iterate_add, ih2],
id               └─────────────┘  └──────┘  └─────────────┘  └─┘
src  ─────┘└────┘└─────────────┘└┘└──────┘└┘└─────────────┘└┘   └─
typ  ─────┘└────┘└─────────────┘└┘└──────┘└┘└─────────────┘└┘└─┘└─
doc  ─────┘└────┘               └┘        └┘               └┘   └─
txt  ─────┘└────┘               └┘        └┘               └┘   └─
par  ─────┘└────┘               └┘        └┘               └┘   └─
pid  ───────────┘               └┘        └┘               └┘   └──
st   ──────────────────────────┘└────────┘└───────────────┘└───┘└──
178        rw [← nat.iterate_add],
id               └─────────────┘
src  ─────┘└────┘└─────────────┘└─
typ  ─────┘└────┘└─────────────┘└─
doc  ─────┘└────┘               └─
txt  ─────┘└────┘               └─
par  ─────┘└────┘               └─
pid  ───────────┘               └──
st   ──────────────────────────┘└──
179        simp only [add_comm, add_left_comm] } },
id                    └──────┘  └───────────┘
src  ─────┘└─────────┘└──────┘└┘└───────────┘└┘└┘
typ  ─────┘└─────────┘└──────┘└┘└───────────┘└┘└┘
doc  ─────┘└─────────┘        └┘             └┘└┘
txt  ─────┘└─────────┘        └┘             └┘└┘
par  ─────┘└─────────┘        └┘             └┘└┘
pid  ────────────────┘        └┘             └─┘
st   ─────────────────────────────────────────┘└┘
180    intro H,
src    └─────┘
typ    └─────┘
doc    └─────┘
txt    └─────┘
par    └─────┘
pid         └┘
st   ────────┘└─
181    cases x with m x,
id           
src    └────┘ └───────┘
typ    └────┘└───────┘
doc    └────┘ └───────┘
txt    └────┘ └───────┘
par    └────┘ └───────┘
pid          └───────┘
st   ─────────────────┘└─
182    cases y with n y,
id           
src    └────┘ └───────┘
typ    └────┘└───────┘
doc    └────┘ └───────┘
txt    └────┘ └───────┘
par    └────┘ └───────┘
pid          └───────┘
st   ─────────────────┘└─
183    cases H with z H, dsimp only at H,
id           
src    └────┘ └───────┘  └─────────────┘
typ    └────┘└───────┘  └─────────────┘
doc    └────┘ └───────┘  └─────────────┘
txt    └────┘ └───────┘  └─────────────┘
par    └────┘ └───────┘  └─────────────┘
pid          └───────┘       └───┘└──┘
st   ─────────────────┘└───────────────┘└─
184    rw [r.sound α p (n+z) m x _ rfl, r.sound α p (m+z) n y _ rfl, H],
id         └─────┘           └─┘  └─────┘           └─┘  
src    └──┘└─────┘      └┘  └─┘└─┘└┘└─────┘      └┘  └─┘└─┘└┘ 
typ    └──┘└─────┘  └┘└─┘└─┘└┘└─────┘  └┘└─┘└─┘└┘
doc    └──┘             └┘  └─┘   └┘             └┘  └─┘   └┘ 
txt    └──┘             └┘  └─┘   └┘             └┘  └─┘   └┘ 
par    └──┘             └┘  └─┘   └┘             └┘  └─┘   └┘ 
pid      └┘             └┘  └─┘   └┘             └┘  └─┘   └┘ 
st   ────────────────────────────────┘└───────────────────────────┘└─┘└──
185    rw [add_assoc, add_comm, add_comm z]
id         └───────┘  └──────┘  └──────┘ 
src    └──┘└───────┘└┘└──────┘└┘└──────┘ └┘
typ    └──┘└───────┘└┘└──────┘└┘└──────┘└┘
doc    └──┘         └┘        └┘         └┘
txt    └──┘         └┘        └┘         └┘
par    └──┘         └┘        └┘         └┘
pid      └┘         └┘        └┘         
st   ──────────────┘└────────┘└──────────┘
186  end
st   └─┘
187  
188  theorem eq_iff [integral_domain α] (p : ℕ) [nat.prime p] [char_p α p]
id                   └─────────────┘           └───────┘    └────┘  
src                  └─────────────┘            └───────┘     └────┘
typ                  └─────────────┘           └───────┘    └────┘  
doc                                              └───────┘     └────┘
189    (x y : ℕ × α) : quot.mk (r α p) x = quot.mk (r α p) y ↔
id                  └─────┘        └─────┘       
src                                                     
typ                 └─────┘        └─────┘       
190      (frobenius α p^[y.1] x.2) = (frobenius α p^[x.1] y.2) :=
id        └───────┘  └┘       └───────┘  └┘  
src       └───────┘    └┘         └───────┘    └┘    
typ       └───────┘  └┘       └───────┘  └┘  
doc       └───────┘                   └───────┘
191  (eq_iff' α p x y).trans ⟨λ ⟨z, H⟩, nat.iterate_inj (frobenius_inj α p) z _ _ $
id    └─────┘     └───┘           └─────────────┘  └───────────┘  
src   └─────┘         └───┘             └─────────────┘  └───────────┘
typ   └─────┘     └───┘           └─────────────┘  └───────────┘  
192    by simpa only [add_comm, nat.iterate_add] using H,
id                    └──────┘  └─────────────┘        
src       └──────────┘└──────┘└┘└─────────────┘└──────┘
typ       └──────────┘└──────┘└┘└─────────────┘└──────┘
doc       └──────────┘        └┘               └──────┘
txt       └──────────┘        └┘               └──────┘
par       └──────────┘        └┘               └──────┘
pid            └──┘└┘        └┘               └────┘
st       └─────────────────────────────────────────────┘
193  λ H, ⟨0, H⟩⟩
id           
typ          
194  
195  instance [discrete_field α] (p : ℕ) [nat.prime p] [char_p α p] : discrete_field (perfect_closure α p) :=
id             └────────────┘           └───────┘    └────┘      └────────────┘  └─────────────┘  
src            └────────────┘            └───────┘     └────┘        └────────────┘  └─────────────┘
typ            └────────────┘           └───────┘    └────┘      └────────────┘  └─────────────┘  
doc                                       └───────┘     └────┘                        └─────────────┘
196  { zero_ne_one := λ H, zero_ne_one ((eq_iff _ _ _ _).1 H),
id                        └─────────┘   └────┘           
src                        └─────────┘   └────┘         
typ                       └─────────┘   └────┘           
197    mul_inv_cancel := λ e, quot.induction_on e $ λ ⟨m, x⟩ H,
id                           └───────────────┘            
src                           └───────────────┘
typ                          └───────────────┘            
198      have _ := mt (eq_iff _ _ _ _).2 H, (eq_iff _ _ _ _).2
id                 └┘  └────┘              └────┘         
src                └┘  └────┘               └────┘         
typ                └┘  └────┘              └────┘         
199        (by simp only [nat.iterate₀ (frobenius_one _ _), nat.iterate₀ (frobenius_zero α p),
id                        └──────────┘  └───────────┘       └──────────┘  └────────────┘  
src            └─────────┘└──────────┘ └───────────┘└─────┘└──────────┘ └────────────┘  └──
typ            └─────────┘└──────────┘ └───────────┘└─────┘└──────────┘ └────────────┘└──
doc            └─────────┘                          └─────┘                             └──
txt            └─────────┘                          └─────┘                             └──
par            └─────────┘                          └─────┘                             └──
pid                └──┘└┘                          └─────┘                             └──
st            └────────────────────────────────────────────────────────────────────────────────
200          nat.iterate_zero, (nat.iterate₂ (frobenius_mul α p)).symm] at this ⊢;
id           └──────────────┘   └──────────┘  └───────────┘  
src  ───────┘└──────────────┘└┘ └──────────┘ └───────────┘  └────────────────┘
typ  ───────┘└──────────────┘└┘ └──────────┘ └───────────┘└────────────────┘
doc  ───────┘                └┘                             └────────────────┘
txt  ───────┘                └┘                             └────────────────┘
par  ───────┘                └┘                             └────────────────┘
pid  ───────┘                └┘                             └──────┘└───────┘
st   ──────────────────────────────────────────────────────────────────────────────
201          rw [mul_inv_cancel this, nat.iterate₀ (frobenius_one _ _)]),
id               └────────────┘ └──┘  └──────────┘  └───────────┘
src          └──┘└────────────┘    └┘└──────────┘ └───────────┘└────┘
typ          └──┘└────────────┘└──┘└┘└──────────┘ └───────────┘└────┘
doc          └──┘                  └┘                          └────┘
txt          └──┘                  └┘                          └────┘
par          └──┘                  └┘                          └────┘
pid            └┘                  └┘                          └────┘
st   ───────────┘└─────────────────┘└────────────────────────────────┘
202    inv_mul_cancel := λ e, quot.induction_on e $ λ ⟨m, x⟩ H,
id                           └───────────────┘            
src                           └───────────────┘
typ                          └───────────────┘            
203      have _ := mt (eq_iff _ _ _ _).2 H, (eq_iff _ _ _ _).2
id                 └┘  └────┘              └────┘         
src                └┘  └────┘               └────┘         
typ                └┘  └────┘              └────┘         
204        (by simp only [nat.iterate₀ (frobenius_one _ _), nat.iterate₀ (frobenius_zero α p),
id                        └──────────┘  └───────────┘       └──────────┘  └────────────┘  
src            └─────────┘└──────────┘ └───────────┘└─────┘└──────────┘ └────────────┘  └──
typ            └─────────┘└──────────┘ └───────────┘└─────┘└──────────┘ └────────────┘└──
doc            └─────────┘                          └─────┘                             └──
txt            └─────────┘                          └─────┘                             └──
par            └─────────┘                          └─────┘                             └──
pid                └──┘└┘                          └─────┘                             └──
st            └────────────────────────────────────────────────────────────────────────────────
205          nat.iterate_zero, (nat.iterate₂ (frobenius_mul α p)).symm] at this ⊢;
id           └──────────────┘   └──────────┘  └───────────┘  
src  ───────┘└──────────────┘└┘ └──────────┘ └───────────┘  └────────────────┘
typ  ───────┘└──────────────┘└┘ └──────────┘ └───────────┘└────────────────┘
doc  ───────┘                └┘                             └────────────────┘
txt  ───────┘                └┘                             └────────────────┘
par  ───────┘                └┘                             └────────────────┘
pid  ───────┘                └┘                             └──────┘└───────┘
st   ──────────────────────────────────────────────────────────────────────────────
206          rw [inv_mul_cancel this, nat.iterate₀ (frobenius_one _ _)]),
id               └────────────┘ └──┘  └──────────┘  └───────────┘
src          └──┘└────────────┘    └┘└──────────┘ └───────────┘└────┘
typ          └──┘└────────────┘└──┘└┘└──────────┘ └───────────┘└────┘
doc          └──┘                  └┘                          └────┘
txt          └──┘                  └┘                          └────┘
par          └──┘                  └┘                          └────┘
pid            └┘                  └┘                          └────┘
st   ───────────┘└─────────────────┘└────────────────────────────────┘
207    has_decidable_eq := λ e f, quot.rec_on_subsingleton e $ λ ⟨m, x⟩,
id                              └──────────────────────┘      
src                               └──────────────────────┘
typ                             └──────────────────────┘      
208      quot.rec_on_subsingleton f $ λ ⟨n, y⟩,
id       └──────────────────────┘      
src      └──────────────────────┘
typ      └──────────────────────┘      
209      decidable_of_iff' _ (eq_iff α p _ _),
id       └───────────────┘    └────┘  
src      └───────────────┘    └────┘
typ      └───────────────┘    └────┘  
210    inv_zero := congr_arg (quot.mk (r α p)) (by rw [inv_zero]),
id                 └───────┘  └─────┘               └──────┘
src                └───────┘                      └──┘└──────┘
typ                └───────┘  └─────┘           └──┘└──────┘
doc                                                └──┘        
txt                                                └──┘        
par                                                └──┘        
pid                                                  └┘        
st                                                └───────────┘
211    .. (infer_instance : has_inv (perfect_closure α p)),
id         └────────────┘   └─────┘  └─────────────┘  
src        └────────────┘   └─────┘  └─────────────┘
typ        └────────────┘   └─────┘  └─────────────┘  
doc        └────────────┘            └─────────────┘
212    .. (infer_instance : comm_ring (perfect_closure α p)) }
id         └────────────┘   └───────┘  └─────────────┘  
src        └────────────┘   └───────┘  └─────────────┘
typ        └────────────┘   └───────┘  └─────────────┘  
doc        └────────────┘              └─────────────┘
213  
214  theorem frobenius_mk [comm_monoid α] (p : ℕ) (x : ℕ × α) :
id                         └─────────┘                 
src                        └─────────┘                 
typ                        └─────────┘                 
215    frobenius (perfect_closure α p) p (quot.mk (r α p) x) = quot.mk _ (x.1, x.2^p) :=
id     └───────┘  └─────────────┘      └─────┘         └─────┘       
src    └───────┘  └─────────────┘                                            
typ    └───────┘  └─────────────┘      └─────┘         └─────┘       
doc    └───────┘  └─────────────┘
216  begin
st   └─────
217    unfold frobenius, cases x with n x, dsimp only,
id                             
src    └──────────────┘  └────┘ └───────┘  └────────┘
typ    └──────────────┘  └────┘└───────┘  └────────┘
doc    └──────────────┘  └────┘ └───────┘  └────────┘
txt    └──────────────┘  └────┘ └───────┘  └────────┘
par    └──────────────┘  └────┘ └───────┘  └────────┘
pid          └────────┘        └───────┘       └───┘
st   ─────────────────┘└────────────────┘└──────────┘└─
218    suffices : ∀ p':ℕ, (quot.mk (r α p) (n, x) ^ p' : perfect_closure α p) = quot.mk (r α p) (n, x ^ p'),
id                                                      └─────────────┘       └─────┘        
src    └─────────┘ └──┘              └┘  └┘ └┘  └─┘└─────────────┘  └┘          └┘ └┘    
typ    └─────────┘ └──┘              └┘  └┘ └┘  └─┘└─────────────┘  └┘└─────┘ └┘└┘   
doc    └─────────┘ └──┘              └┘  └┘ └┘   └─┘└─────────────┘  └┘            └┘  └┘    
txt    └─────────┘ └──┘              └┘  └┘ └┘   └─┘                 └┘            └┘  └┘    
par    └─────────┘ └──┘              └┘  └┘ └┘   └─┘                 └┘            └┘  └┘    
pid    └───────┘└┘ └──┘              └┘  └┘ └┘   └─┘                 └┘            └┘  └┘    
st   ─────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
219    { apply this },
src      └────┘    
typ      └────┘    
doc      └────┘    
txt      └────┘    
par      └────┘    
pid               
st   ───┘└─────────┘└┘
220    intro p, induction p with p ih,
id                        
src    └─────┘  └────────┘ └────────┘
typ    └─────┘  └────────┘└────────┘
doc    └─────┘  └────────┘ └────────┘
txt    └─────┘  └────────┘ └────────┘
par    └─────┘  └────────┘ └────────┘
pid         └┘            └───────┘
st   ────────┘└─────────────────────┘└─
221    case nat.zero { apply r.sound, rw [nat.iterate₀ (frobenius_one _ _), pow_zero] },
id                           └─────┘      └──────────┘  └───────────┘       └──────┘
src    └──────────────┘└────┘└─────┘└┘└──┘└──────────┘ └───────────┘└─────┘└──────┘└┘
typ    └──────────────┘└────┘└─────┘└┘└──┘└──────────┘ └───────────┘└─────┘└──────┘└┘
doc    └──────────────┘└────┘       └┘└──┘                          └─────┘        └┘
txt    └──────────────┘└────┘       └┘└──┘                          └─────┘        └┘
par    └──────────────┘└────┘       └┘└──┘                          └─────┘        └┘
pid        └───────┘└──────┘       └────┘                          └─────┘        └─┘
st   ────────────────┘└────────────┘└────────────────────────────────────┘└────────┘└┘
222    case nat.succ {
src    └───────────────
typ    └───────────────
doc    └───────────────
txt    └───────────────
par    └───────────────
pid        └───────┘└─
st   ──────────────────
223      rw [pow_succ, ih],
id           └──────┘  └┘
src  ───┘└──┘└──────┘└┘  └─
typ  ───┘└──┘└──────┘└┘└┘└─
doc  ───┘└──┘        └┘  └─
txt  ───┘└──┘        └┘  └─
par  ───┘└──┘        └┘  └─
pid  ───────┘        └┘  └──
st   ───────────────┘└──┘└─
224      symmetry,
src  ───┘└──────┘└─
typ  ───┘└──────┘└─
doc  ───┘└──────┘└─
txt  ───┘└──────┘└─
par  ───┘└──────┘└─
pid  ──────────────
st   ───────────┘└─
225      apply r.sound,
id             └─────┘
src  ───┘└────┘└─────┘└─
typ  ───┘└────┘└─────┘└─
doc  ───┘└────┘       └─
txt  ───┘└────┘       └─
par  ───┘└────┘       └─
pid  ─────────┘       └─
st   ────────────────┘└─
226      simp only [pow_succ, nat.iterate₂ (frobenius_mul _ _)]
id                  └──────┘  └──────────┘  └───────────┘
src  ───┘└─────────┘└──────┘└┘└──────────┘ └───────────┘└──────
typ  ───┘└─────────┘└──────┘└┘└──────────┘ └───────────┘└──────
doc  ───┘└─────────┘        └┘                          └──────
txt  ───┘└─────────┘        └┘                          └──────
par  ───┘└─────────┘        └┘                          └──────
pid  ──────────────┘        └┘                          └──────
st   ───────────────────────────────────────────────────────────
227    }
src  ─┘└┘
typ  ─┘└┘
doc  ─┘└┘
txt  ─┘└┘
par  ─┘└┘
pid  ──┘
st   ─┘
228  end
st   └─┘
229  
230  def frobenius_equiv [comm_ring α] (p : ℕ) [nat.prime p] [char_p α p] :
id                        └───────┘           └───────┘    └────┘  
src                       └───────┘            └───────┘     └────┘
typ                       └───────┘           └───────┘    └────┘  
doc                                             └───────┘     └────┘
231    perfect_closure α p ≃ perfect_closure α p :=
id     └─────────────┘    └─────────────┘  
src    └─────────────┘      └─────────────┘
typ    └─────────────┘    └─────────────┘  
doc    └─────────────┘      └─────────────┘
232  { to_fun := frobenius (perfect_closure α p) p,
id               └───────┘  └─────────────┘    
src              └───────┘  └─────────────┘
typ              └───────┘  └─────────────┘    
doc              └───────┘  └─────────────┘
233    inv_fun := λ e, quot.lift_on e (λ x, quot.mk (r α p) (x.1 + 1, x.2)) (λ x y H,
id                    └──────────┘       └─────┘                     
src                    └──────────┘                                
typ                   └──────────┘       └─────┘                     
234      match x, y, H with
id                 
typ                
235      | _, _, r.intro _ n x := quot.sound (r.intro _ _ _)
id               └─────┘          └────────┘  └─────┘
src              └─────┘          └────────┘  └─────┘
typ              └─────┘          └────────┘  └─────┘
236      end),
237    left_inv := λ e, quot.induction_on e (λ ⟨m, x⟩, by rw frobenius_mk;
id                     └───────────────┘                  └──────────┘
src                     └───────────────┘                 └─┘└──────────┘
typ                    └───────────────┘               └─┘└──────────┘
doc                                                       └─┘
txt                                                       └─┘
par                                                       └─┘
pid                                                         
st                                                       └─────────────────
238      symmetry; apply quot.sound; apply r.intro),
id                       └────────┘        └─────┘
src      └──────┘  └────┘└────────┘  └────┘└─────┘
typ      └──────┘  └────┘└────────┘  └────┘└─────┘
doc      └──────┘  └────┘            └────┘
txt      └──────┘  └────┘            └────┘
par      └──────┘  └────┘            └────┘
pid                                      
st   ────────────────────────────────────────────┘
239    right_inv := λ e, quot.induction_on e (λ ⟨m, x⟩, by rw frobenius_mk;
id                      └───────────────┘                  └──────────┘
src                      └───────────────┘                 └─┘└──────────┘
typ                     └───────────────┘               └─┘└──────────┘
doc                                                        └─┘
txt                                                        └─┘
par                                                        └─┘
pid                                                          
st                                                        └─────────────────
240      symmetry; apply quot.sound; apply r.intro) }
id                       └────────┘        └─────┘
src      └──────┘  └────┘└────────┘  └────┘└─────┘
typ      └──────┘  └────┘└────────┘  └────┘└─────┘
doc      └──────┘  └────┘            └────┘
txt      └──────┘  └────┘            └────┘
par      └──────┘  └────┘            └────┘
pid                                      
st   ────────────────────────────────────────────┘
241  
242  theorem frobenius_equiv_apply [comm_ring α] (p : ℕ) [nat.prime p] [char_p α p] {x : perfect_closure α p} :
id                                  └───────┘           └───────┘    └────┘         └─────────────┘  
src                                 └───────┘            └───────┘     └────┘           └─────────────┘
typ                                 └───────┘           └───────┘    └────┘         └─────────────┘  
doc                                                       └───────┘     └────┘           └─────────────┘
243    frobenius_equiv α p x = frobenius _ p x :=
id     └─────────────┘     └───────┘    
src    └─────────────┘        └───────┘
typ    └─────────────┘     └───────┘    
doc                            └───────┘
244  rfl
id   └─┘
src  └─┘
typ  └─┘
245  
246  theorem nat_cast [comm_ring α] (p : ℕ) [nat.prime p] [char_p α p] (n x : ℕ) :
id                     └───────┘           └───────┘    └────┘           
src                    └───────┘            └───────┘     └────┘             
typ                    └───────┘           └───────┘    └────┘           
doc                                          └───────┘     └────┘
247    (x : perfect_closure α p) = quot.mk (r α p) (n, x) :=
id         └─────────────┘     └─────┘        
src         └─────────────┘                      
typ        └─────────────┘     └─────┘        
doc         └─────────────┘
248  begin
st   └─────
249    induction n with n ih,
id               
src    └────────┘ └────────┘
typ    └────────┘└────────┘
doc    └────────┘ └────────┘
txt    └────────┘ └────────┘
par    └────────┘ └────────┘
pid              └───────┘
st   ──────────────────────┘└─
250    { induction x with x ih, {refl},
id                 
src      └────────┘ └────────┘   └──┘
typ      └────────┘└────────┘   └──┘
doc      └────────┘ └────────┘   └──┘
txt      └────────┘ └────────┘   └──┘
par      └────────┘ └────────┘   └──┘
pid                └───────┘
st   ───┘└───────────────────┘└─────┘└┘
251      rw [nat.cast_succ, nat.cast_succ, ih], refl },
id           └───────────┘  └───────────┘  └┘
src      └──┘└───────────┘└┘└───────────┘└┘    └───┘
typ      └──┘└───────────┘└┘└───────────┘└┘└┘  └───┘
doc      └──┘             └┘             └┘    └───┘
txt      └──┘             └┘             └┘    └───┘
par      └──┘             └┘             └┘    └───┘
pid        └┘             └┘             └┘        
st   ────────────────────┘└─────────────┘└──┘└─────┘└┘
252    rw ih, apply quot.sound,
id        └┘        └────────┘
src    └─┘    └────┘└────────┘
typ    └─┘└┘  └────┘└────────┘
doc    └─┘    └────┘
txt    └─┘    └────┘
par    └─┘    └────┘
pid               
st   ──────┘└────────────────┘└─
253    conv {congr, skip, skip, rw ← frobenius_nat_cast α p x},
id                                   └────────────────┘   
src    └────┘└───┘└┘└──┘└┘└──┘└┘└───┘└────────────────┘   
typ    └────┘└───┘└┘└──┘└┘└──┘└┘└───┘└────────────────┘
txt    └────┘└───┘└┘└──┘└┘└──┘└┘└───┘                     
par    └────┘└───┘└┘└──┘└┘└──┘└┘└───┘                     
pid        └───────────────────────┘                     
st   ───────┘└───┘└────┘└────┘└─────────────────────────────┘└┘
254    apply r.intro
id           └─────┘
src    └────┘└─────┘
typ    └────┘└─────┘
doc    └────┘       
txt    └────┘       
par    └────┘       
pid                
st   ───────────────┘
255  end
st   └─┘
256  
257  theorem int_cast [comm_ring α] (p : ℕ) [nat.prime p] [char_p α p] (x : ℤ) :
id                     └───────┘           └───────┘    └────┘         
src                    └───────┘            └───────┘     └────┘           
typ                    └───────┘           └───────┘    └────┘         
doc                                          └───────┘     └────┘
258    (x : perfect_closure α p) = quot.mk (r α p) (0, x) :=
id         └─────────────┘     └─────┘         
src         └─────────────┘                      
typ        └─────────────┘     └─────┘         
doc         └─────────────┘
259  by induction x; simp only [int.cast_of_nat, int.cast_neg_succ_of_nat, nat_cast α p 0]; refl
id                             └─────────────┘  └──────────────────────┘  └──────┘  
src     └────────┘   └─────────┘└─────────────┘└┘└──────────────────────┘└┘└──────┘  └─┘  └────
typ     └────────┘  └─────────┘└─────────────┘└┘└──────────────────────┘└┘└──────┘└─┘  └────
doc     └────────┘   └─────────┘               └┘                        └┘          └─┘  └────
txt     └────────┘   └─────────┘               └┘                        └┘          └─┘  └────
par     └────────┘   └─────────┘               └┘                        └┘          └─┘  └────
pid                     └──┘└┘               └┘                        └┘          └─┘      
st     └─────────────────────────────────────────────────────────────────────────────────────────
260  
src  
typ  
doc  
txt  
par  
pid  
st   
261  theorem nat_cast_eq_iff [comm_ring α] (p : ℕ) [nat.prime p] [char_p α p] (x y : ℕ) :
id                            └───────┘           └───────┘    └────┘           
src                           └───────┘            └───────┘     └────┘             
typ                           └───────┘           └───────┘    └────┘           
doc                                                 └───────┘     └────┘
262    (x : perfect_closure α p) = y ↔ (x : α) = y :=
id         └─────────────┘              
src         └─────────────┘                  
typ        └─────────────┘              
doc         └─────────────┘
263  begin
st   └─────
264    split; intro H,
src    └───┘  └─────┘
typ    └───┘  └─────┘
doc    └───┘  └─────┘
txt    └───┘  └─────┘
par    └───┘  └─────┘
pid                └┘
st   ───────────────┘└─
265    { rw [nat_cast α p 0, nat_cast α p 0, eq_iff'] at H,
id           └──────┘      └──────┘      └─────┘
src      └──┘└──────┘  └──┘└──────┘  └──┘└─────┘└────┘
typ      └──┘└──────┘└──┘└──────┘└──┘└─────┘└────┘
doc      └──┘          └──┘          └──┘       └────┘
txt      └──┘          └──┘          └──┘       └────┘
par      └──┘          └──┘          └──┘       └────┘
pid        └┘          └──┘          └──┘       └───┘
st   ───┘└───────────────┘└──────────────┘└────────┘└───┘└─
266      cases H with z H,
id             
src      └────┘ └───────┘
typ      └────┘└───────┘
doc      └────┘ └───────┘
txt      └────┘ └───────┘
par      └────┘ └───────┘
pid            └───────┘
st   ───────────────────┘└─
267      simpa only [zero_add, nat.iterate₀ (frobenius_nat_cast α p _)] using H },
id                   └──────┘  └──────────┘  └────────────────┘             
src      └──────────┘└──────┘└┘└──────────┘ └────────────────┘  └─────────┘ 
typ      └──────────┘└──────┘└┘└──────────┘ └────────────────┘└─────────┘
doc      └──────────┘        └┘                                 └─────────┘ 
txt      └──────────┘        └┘                                 └─────────┘ 
par      └──────────┘        └┘                                 └─────────┘ 
pid           └──┘└┘        └┘                                 └──┘└────┘ 
st   ──────────────────────────────────────────────────────────────────────────┘└┘
268    rw [nat_cast α p 0, nat_cast α p 0, H]
id         └──────┘      └──────┘      
src    └──┘└──────┘  └──┘└──────┘  └──┘ └┘
typ    └──┘└──────┘└──┘└──────┘└──┘└┘
doc    └──┘          └──┘          └──┘ └┘
txt    └──┘          └──┘          └──┘ └┘
par    └──┘          └──┘          └──┘ └┘
pid      └┘          └──┘          └──┘ 
st   ──────────────────┘└──────────────┘└──┘
269  end
st   └─┘
270  
271  instance [comm_ring α] (p : ℕ) [nat.prime p] [char_p α p] : char_p (perfect_closure α p) p :=
id             └───────┘           └───────┘    └────┘      └────┘  └─────────────┘    
src            └───────┘            └───────┘     └────┘        └────┘  └─────────────┘
typ            └───────┘           └───────┘    └────┘      └────┘  └─────────────┘    
doc                                  └───────┘     └────┘        └────┘  └─────────────┘
272  begin
st   └─────
273    constructor, intro x, rw ← char_p.cast_eq_zero_iff α,
id                                └─────────────────────┘ 
src    └─────────┘  └─────┘  └───┘└─────────────────────┘
typ    └─────────┘  └─────┘  └───┘└─────────────────────┘
doc    └─────────┘  └─────┘  └───┘                       
txt    └─────────┘  └─────┘  └───┘                       
par    └─────────┘  └─────┘  └───┘                       
pid                      └┘    └─┘                       
st   ────────────┘└───────┘└──────────────────────────────┘└─
274    rw [← nat.cast_zero, nat_cast_eq_iff, nat.cast_zero]
id           └───────────┘  └─────────────┘  └───────────┘
src    └────┘└───────────┘└┘└─────────────┘└┘└───────────┘└┘
typ    └────┘└───────────┘└┘└─────────────┘└┘└───────────┘└┘
doc    └────┘             └┘               └┘             └┘
txt    └────┘             └┘               └┘             └┘
par    └────┘             └┘               └┘             └┘
pid      └──┘             └┘               └┘             
st   ────────────────────┘└───────────────┘└─────────────┘
275  end
st   └─┘
276  
277  instance [discrete_field α] (p : ℕ) [nat.prime p] [char_p α p] : perfect_field (perfect_closure α p) p :=
id             └────────────┘           └───────┘    └────┘      └───────────┘  └─────────────┘    
src            └────────────┘            └───────┘     └────┘        └───────────┘  └─────────────┘
typ            └────────────┘           └───────┘    └────┘      └───────────┘  └─────────────┘    
doc                                       └───────┘     └────┘        └───────────┘  └─────────────┘
278  { pth_root := (frobenius_equiv α p).symm,
id                  └─────────────┘   └──┘
src                 └─────────────┘     └──┘
typ                 └─────────────┘   └──┘
279    frobenius_pth_root := (frobenius_equiv α p).apply_symm_apply }
id                            └─────────────┘   └──────────────┘
src                           └─────────────┘     └──────────────┘
typ                           └─────────────┘   └──────────────┘
280  
281  def of [monoid α] (p : ℕ) (x : α) : perfect_closure α p :=
id           └────┘                   └─────────────┘  
src          └────┘                     └─────────────┘
typ          └────┘                   └─────────────┘  
doc                                      └─────────────┘
282  quot.mk _ (0, x)
id   └─────┘      
src            
typ  └─────┘      
283  
284  instance [comm_ring α] (p : ℕ) [nat.prime p] [char_p α p] : is_ring_hom (of α p) :=
id             └───────┘           └───────┘    └────┘      └─────────┘  └┘  
src            └───────┘            └───────┘     └────┘        └─────────┘  └┘
typ            └───────┘           └───────┘    └────┘      └─────────┘  └┘  
doc                                  └───────┘     └────┘        └─────────┘
285  { map_one := rfl,
id                └─┘
src               └─┘
typ               └─┘
286    map_mul := λ x y, rfl,
id                     └─┘
src                      └─┘
typ                    └─┘
287    map_add := λ x y, rfl }
id                     └─┘
src                      └─┘
typ                    └─┘
288  
289  theorem eq_pth_root [discrete_field α] (p : ℕ) [nat.prime p] [char_p α p] (m : ℕ) (x : α) :
id                        └────────────┘           └───────┘    └────┘                
src                       └────────────┘            └───────┘     └────┘           
typ                       └────────────┘           └───────┘    └────┘                
doc                                                  └───────┘     └────┘
290    quot.mk (r α p) (m, x) = (perfect_field.pth_root p^[m] (of α p x) : perfect_closure α p) :=
id     └─────┘            └────────────────────┘ └┘  └┘       └─────────────┘  
src                           └────────────────────┘  └┘   └┘          └─────────────┘
typ    └─────┘            └────────────────────┘ └┘  └┘       └─────────────┘  
doc                                                                        └─────────────┘
291  begin
st   └─────
292    unfold of,
src    └───────┘
typ    └───────┘
doc    └───────┘
txt    └───────┘
par    └───────┘
pid          └─┘
st   ──────────┘└─
293    induction m with m ih, {refl},
id               
src    └────────┘ └────────┘   └──┘
typ    └────────┘└────────┘   └──┘
doc    └────────┘ └────────┘   └──┘
txt    └────────┘ └────────┘   └──┘
par    └────────┘ └────────┘   └──┘
pid              └───────┘
st   ──────────────────────┘└─────┘└┘
294    rw [nat.iterate_succ', ← ih]; refl
id         └───────────────┘    └┘
src    └──┘└───────────────┘└──┘    └───┘
typ    └──┘└───────────────┘└──┘└┘  └───┘
doc    └──┘                 └──┘    └───┘
txt    └──┘                 └──┘    └───┘
par    └──┘                 └──┘    └───┘
pid      └┘                 └──┘        
st   ──────────────────────┘└────┘└─────┘
295  end
st   └─┘
296  
297  def UMP [discrete_field α] (p : ℕ) [nat.prime p] [char_p α p]
id            └────────────┘           └───────┘    └────┘  
src           └────────────┘            └───────┘     └────┘
typ           └────────────┘           └───────┘    └────┘  
doc                                      └───────┘     └────┘
298    (β : Type v) [discrete_field β] [char_p β p] [perfect_field β p] :
id                   └────────────┘    └────┘     └───────────┘  
src                  └────────────┘     └────┘       └───────────┘
typ                  └────────────┘    └────┘     └───────────┘  
doc                                     └────┘       └───────────┘
299    { f : α → β // is_ring_hom f } ≃ { f : perfect_closure α p → β // is_ring_hom f } :=
id                └─────────┘          └─────────────┘        └─────────┘ 
src                  └─────────┘           └─────────────┘            └─────────┘
typ               └─────────┘          └─────────────┘        └─────────┘ 
doc                   └─────────┘            └─────────────┘            └─────────┘
300  { to_fun := λ f, ⟨λ e, quot.lift_on e (λ x, perfect_field.pth_root p^[x.1] (f.1 x.2))
id                        └──────────┘       └────────────────────┘ └┘     
src                         └──────────┘         └────────────────────┘  └┘        
typ                       └──────────┘       └────────────────────┘ └┘     
301        (λ x y H, match x, y, H with | _, _, r.intro _ n x := by letI := f.2;
id                                        └─────┘                     
src                                             └─────┘             └──────┘ └┘
typ                                       └─────┘             └──────┘└┘
doc                                                                 └──────┘ └┘
txt                                                                 └──────┘ └┘
par                                                                 └──────┘ └┘
pid                                                                     └─┘ └┘
st                                                                 └─────────────
302          simp only [is_monoid_hom.map_frobenius f.1, nat.iterate_succ, pth_root_frobenius]
id                      └─────────────────────────┘     └──────────────┘  └────────────────┘
src          └─────────┘└─────────────────────────┘ └──┘└──────────────┘└┘└────────────────┘└─
typ          └─────────┘└─────────────────────────┘└──┘└──────────────┘└┘└────────────────┘└─
doc          └─────────┘                            └──┘                └┘                  └─
txt          └─────────┘                            └──┘                └┘                  └─
par          └─────────┘                            └──┘                └┘                  └─
pid              └──┘└┘                            └──┘                └┘                  
st   ──────────────────────────────────────────────────────────────────────────────────────────
303        end),
src  ─────┘
typ  ─────┘
doc  ─────┘
txt  ─────┘
par  ─────┘
pid  ─────┘
st   ─────┘
304      show f.1 1 = 1, from f.2.1,
id                          
src                           
typ                         
305      λ j k, quot.induction_on j $ λ ⟨m, x⟩, quot.induction_on k $ λ ⟨n, y⟩,
id            └───────────────┘             └───────────────┘      
src             └───────────────┘               └───────────────┘
typ           └───────────────┘             └───────────────┘      
306        show (perfect_field.pth_root p^[_] _) = (perfect_field.pth_root p^[_] _) * (perfect_field.pth_root p^[_] _),
id               └────────────────────┘ └┘       └────────────────────┘ └┘       └────────────────────┘ └┘ 
src              └────────────────────┘  └┘       └────────────────────┘  └┘       └────────────────────┘  └┘ 
typ              └────────────────────┘ └┘       └────────────────────┘ └┘       └────────────────────┘ └┘ 
307        by letI := f.2; simp only [is_ring_hom.map_mul f.1, (nat.iterate₁ (λ x, (is_monoid_hom.map_frobenius f.1 p x).symm)).symm,
id                                   └─────────────────┘      └──────────┘        └─────────────────────────┘    
src           └──────┘ └┘  └─────────┘└─────────────────┘ └──┘ └──────────┘  └──┘ └─────────────────────────┘ └─┘  └──────────────
typ           └──────┘└┘  └─────────┘└─────────────────┘└──┘ └──────────┘  └──┘ └─────────────────────────┘└─┘ └──────────────
doc           └──────┘ └┘  └─────────┘                    └──┘               └──┘                             └─┘  └──────────────
txt           └──────┘ └┘  └─────────┘                    └──┘               └──┘                             └─┘  └──────────────
par           └──────┘ └┘  └─────────┘                    └──┘               └──┘                             └─┘  └──────────────
pid               └─┘ └┘      └──┘└┘                    └──┘               └──┘                             └─┘  └──────────────
st           └────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────
308            @nat.iterate₂ β _ (*) (λ x y, is_ring_hom.map_mul (perfect_field.pth_root p))];
id              └──────────┘               └─────────────────┘  └────────────────────┘ 
src  ─────────┘ └──────────┘ └─┘└─┘  └────┘└─────────────────┘ └────────────────────┘ └─┘
typ  ─────────┘ └──────────┘└─┘└─┘  └────┘└─────────────────┘ └────────────────────┘└─┘
doc  ─────────┘              └─┘ └─┘  └────┘                                           └─┘
txt  ─────────┘              └─┘ └─┘  └────┘                                           └─┘
par  ─────────┘              └─┘ └─┘  └────┘                                           └─┘
pid  ─────────┘              └─┘ └─┘  └────┘                                           └─┘
st   ──────────────────────────────────────────────────────────────────────────────────────────
309          rw [nat.iterate_add, nat.iterate_cancel (pth_root_frobenius β p),
id               └─────────────┘  └────────────────┘  └────────────────┘  
src          └──┘└─────────────┘└┘└────────────────┘ └────────────────┘  └──
typ          └──┘└─────────────┘└┘└────────────────┘ └────────────────┘└──
doc          └──┘               └┘                                       └──
txt          └──┘               └┘                                       └──
par          └──┘               └┘                                       └──
pid            └┘               └┘                                       └──
st   ───────────┘└─────────────┘└───────────────────────────────────────────┘└─
310            add_comm, nat.iterate_add, nat.iterate_cancel (pth_root_frobenius β p)],
id             └──────┘  └─────────────┘  └────────────────┘  └────────────────┘  
src  ─────────┘└──────┘└┘└─────────────┘└┘└────────────────┘ └────────────────┘  └┘
typ  ─────────┘└──────┘└┘└─────────────┘└┘└────────────────┘ └────────────────┘└┘
doc  ─────────┘        └┘               └┘                                       └┘
txt  ─────────┘        └┘               └┘                                       └┘
par  ─────────┘        └┘               └┘                                       └┘
pid  ─────────┘        └┘               └┘                                       └┘
st   ─────────────────┘└───────────────┘└───────────────────────────────────────────┘
311      λ j k, quot.induction_on j $ λ ⟨m, x⟩, quot.induction_on k $ λ ⟨n, y⟩,
id            └───────────────┘             └───────────────┘      
src             └───────────────┘               └───────────────┘
typ           └───────────────┘             └───────────────┘      
312        show (perfect_field.pth_root p^[_] _) = (perfect_field.pth_root p^[_] _) + (perfect_field.pth_root p^[_] _),
id               └────────────────────┘ └┘       └────────────────────┘ └┘       └────────────────────┘ └┘ 
src              └────────────────────┘  └┘       └────────────────────┘  └┘       └────────────────────┘  └┘ 
typ              └────────────────────┘ └┘       └────────────────────┘ └┘       └────────────────────┘ └┘ 
313        by letI := f.2; simp only [is_ring_hom.map_add f.1, (nat.iterate₁ (λ x, (is_monoid_hom.map_frobenius f.1 p x).symm)).symm,
id                                   └─────────────────┘      └──────────┘        └─────────────────────────┘    
src           └──────┘ └┘  └─────────┘└─────────────────┘ └──┘ └──────────┘  └──┘ └─────────────────────────┘ └─┘  └──────────────
typ           └──────┘└┘  └─────────┘└─────────────────┘└──┘ └──────────┘  └──┘ └─────────────────────────┘└─┘ └──────────────
doc           └──────┘ └┘  └─────────┘                    └──┘               └──┘                             └─┘  └──────────────
txt           └──────┘ └┘  └─────────┘                    └──┘               └──┘                             └─┘  └──────────────
par           └──────┘ └┘  └─────────┘                    └──┘               └──┘                             └─┘  └──────────────
pid               └─┘ └┘      └──┘└┘                    └──┘               └──┘                             └─┘  └──────────────
st           └────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────
314            @nat.iterate₂ β _ (+) (λ x y, is_ring_hom.map_add (perfect_field.pth_root p))];
id              └──────────┘               └─────────────────┘  └────────────────────┘ 
src  ─────────┘ └──────────┘ └─┘└─┘  └────┘└─────────────────┘ └────────────────────┘ └─┘
typ  ─────────┘ └──────────┘└─┘└─┘  └────┘└─────────────────┘ └────────────────────┘└─┘
doc  ─────────┘              └─┘ └─┘  └────┘                                           └─┘
txt  ─────────┘              └─┘ └─┘  └────┘                                           └─┘
par  ─────────┘              └─┘ └─┘  └────┘                                           └─┘
pid  ─────────┘              └─┘ └─┘  └────┘                                           └─┘
st   ──────────────────────────────────────────────────────────────────────────────────────────
315          rw [nat.iterate_add, nat.iterate_cancel (pth_root_frobenius β p),
id               └─────────────┘  └────────────────┘  └────────────────┘  
src          └──┘└─────────────┘└┘└────────────────┘ └────────────────┘  └──
typ          └──┘└─────────────┘└┘└────────────────┘ └────────────────┘└──
doc          └──┘               └┘                                       └──
txt          └──┘               └┘                                       └──
par          └──┘               └┘                                       └──
pid            └┘               └┘                                       └──
st   ───────────┘└─────────────┘└───────────────────────────────────────────┘└─
316            add_comm m, nat.iterate_add, nat.iterate_cancel (pth_root_frobenius β p)]⟩,
id             └──────┘   └─────────────┘  └────────────────┘  └────────────────┘  
src  ─────────┘└──────┘ └┘└─────────────┘└┘└────────────────┘ └────────────────┘  └┘
typ  ─────────┘└──────┘└┘└─────────────┘└┘└────────────────┘ └────────────────┘└┘
doc  ─────────┘         └┘               └┘                                       └┘
txt  ─────────┘         └┘               └┘                                       └┘
par  ─────────┘         └┘               └┘                                       └┘
pid  ─────────┘         └┘               └┘                                       └┘
st   ───────────────────┘└───────────────┘└───────────────────────────────────────────┘
317    inv_fun := λ f, ⟨f.1 ∘ of α p, @@is_ring_hom.comp _ _ _ _ _ _ f.2⟩,
id                        └┘      └──────────────┘             
src                         └┘        └──────────────┘              
typ                       └┘      └──────────────┘             
doc                                     └──────────────┘
318    left_inv := λ ⟨f, hf⟩, subtype.eq rfl,
id                           └────────┘ └─┘
src                           └────────┘ └─┘
typ                          └────────┘ └─┘
319    right_inv := λ ⟨f, hf⟩, subtype.eq $ funext $ λ i, quot.induction_on i $ λ ⟨m, x⟩,
id                           └────────┘   └────┘       └───────────────┘      
src                            └────────┘   └────┘        └───────────────┘
typ                          └────────┘   └────┘       └───────────────┘      
320      show perfect_field.pth_root p^[m] (f _) = f _,
id            └────────────────────┘ └┘        
src           └────────────────────┘  └┘        
typ           └────────────────────┘ └┘        
321      by resetI; rw [eq_pth_root, @nat.iterate₁ _ _ _ _ f (λ x:perfect_closure α p, (is_ring_hom.pth_root p f).symm)] }
id                      └─────────┘   └──────────┘                └─────────────┘      └──────────────────┘  
src         └────┘  └──┘└─────────┘└┘ └──────────┘└───────┘   └─┘└─────────────┘  └┘ └──────────────────┘  └───────┘
typ         └────┘  └──┘└─────────┘└┘ └──────────┘└───────┘   └─┘└─────────────┘ └┘ └──────────────────┘└───────┘
doc         └────┘  └──┘           └┘             └───────┘   └─┘└─────────────┘  └┘                       └───────┘
txt         └────┘  └──┘           └┘             └───────┘   └─┘                 └┘                       └───────┘
par         └────┘  └──┘           └┘             └───────┘   └─┘                 └┘                       └───────┘
pid                   └┘           └┘             └───────┘   └─┘                 └┘                       └──────┘
st         └──────────────────────┘└──────────────────────────────────────────────────────────────────────────────────┘
322  
323  end perfect_closure